Inference at * 1 2 1 1 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. i : {0..(||L1 @ L2|| - 1)}
7. x = (L1 @ L2)[i]
8. y = (L1 @ L2)[(i+1)]
9. (i < ||L1||)
  x = L2[(i - ||L1||)] 

latex

 by ((RWO "select_append_back" (-3)) 
CollapseTHEN (((Auto') 
CollapseTHEN (((All ArithSimp) 

CoCollapseTHEN (Auto)))))) 

latex

C.

Definitions	P  Q, P  Q, l[i], t  T, i  j < k, P & Q, x:A  B(x), Void, #$n, False, P  Q, a < b, n - m, -n, n+m, A, {x:A| B(x)} , , type List, Type, {i..j}, ||as||, as @ bs, i  j , A  B, x:A. B(x), x:AB(x), s = t
Lemmas	iff wf, rev implies wf, select append back, le wf, append wf, non neg length, length append